COMMENT ⊗   VALID 00002 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	
C00007 ENDMK
C⊗;

% Axioms for extensional forms %
AXIOM EXTFORM:

∀e.(isextform(e) ⊃ isset(dom(e)));

∀e.(isextform(e) ⊃ isset(vars(e)));

∀e.(isextform(e) ⊃ (∀x.xεvars(e)⊃isvar(x)));

∀v.(isvar(v) ⊃ isextform(v));

∀v.(isvar(v) ⊃ vars(v)={v});

∀s.(isstate(s) ≡ ismap(s) ∧ ∀x.(xεdomain(s) ⊃ isvar(x) ∧ ap(s,x)εdom(x)));

∀s x u.(isstate(s)∧isvar(x)∧uεdom(x) ⊃ isstate(assign(x,u,s)));

∀s x u.(isstate(s)∧isvar(x)∧uεdom(x) ⊃ domain(assign(x,u,s))={x}∪domain(s));

∀s x u.(isstate(s)∧isvar(x)∧uεdom(x) ⊃ ap(assign(x,u,s),x)=u);

∀s x u.(isstate(s)∧isvar(x)∧uεdom(x) ⊃ ∀v.(¬v=x ∧ vεdomain(s)
	⊃ ap(assign(x,u,s),v)=ap(s,v)));

∀s e.(isstate(s)∧isextform(e)∧vars(e)⊂domain(s) ⊃ value(e,s)εdom(e));

∀s x.(isstate(s)∧isvar(x) ⊃ value(x,s)=ap(s,x));

CONST:

∀x y.(xεy ⊃ isextform(mkconst(x,y)));

∀x y.(xεy ⊃ dom(mkconst(x,y))=y);

∀x y.(xεy ⊃ vars(mkconst(x,y))=NULLSET);

∀x y.(xεy ⊃ ∀s.(isstate(s) ⊃ value(mkconst(x,y),s)=x));

APP:

∀f e u v.(isextform(f)∧isextform(e)∧dom(f)=(u→v)∧dom(e)=u ⊃ isextform(ap2(f,e)));

∀f e u v.(isextform(f)∧isextform(e)∧dom(f)=(u→v)∧dom(e)=u ⊃ dom(ap2(f,e))=v);

∀f e u v.(isextform(f)∧isextform(e)∧dom(f)=(u→v)∧dom(e)=u ⊃ 
	vars(ap2(f,e)) ⊂ vars(f)∪vars(e));

∀f e u v.(isextform(f)∧isextform(e)∧dom(f)=(u→v)∧dom(e)=u
	⊃ ∀s.(isstate(s) ∧ (vars(f) ⊂ domain(s)) ∧ (vars(e) ⊂ domain(s))
		⊃ value(ap2(f,e),s) = ap(value(f,s),value(e,s))));

EXTEN:

∀e1 e2.(isextform(e1)∧isextform(e2)
	∧ ∀s.(isstate(s) ∧ vars(e1)⊂domain(s)∧vars(e2)⊂domain(s) ⊃
			value(e1,s)=value(e2,s)) ⊃ e1=e2);

EXTEND:
∀s1 s2.(isstate(s1)∧isstate(s2) ⊃ (extends(s1,s2) ≡
		domain(s2)⊂domain(s1) ∧ ∀x.(xεdomain(s2) ⊃ ap(s1,x)=ap(s2,x))));

∀e s1 s2.(isextform(e)∧isstate(s1)∧isstate(s2)∧vars(e)⊂domain(s2)∧extends(s1,s2)
		⊃ value(e,s1)=value(e,s2));

LAMBDA:

∀ x e.(isvar(x)∧isextform(e) ⊃ isextform(lambda(x,e)));

∀ x e.(isvar(x)∧isextform(e) ⊃ dom(lambda(x,e))=(dom(x)→dom(e)));

∀ x e.(isvar(x)∧isextform(e) ⊃ vars(lambda(x,e))⊂vars(e)-{x});

∀ x e.(isvar(x)∧isextform(e) ⊃ ∀s.(isstate(s)∧vars(lambda(x,e))⊂domain(s)
		⊃ ∀y.(yεdom(x) ⊃ ap(value(lambda(x,e),s),y)
			= value(e,assign(x,y,s)))));

SUBST:

∀e1 x e2.(isextform(e1)∧isvar(x)∧isextform(e2)∧dom(e1)=dom(x) ⊃
	isextform(subst(e1,x,e2)));

∀e1 x e2.(isextform(e1)∧isvar(x)∧isextform(e2)∧dom(e1)=dom(x) ⊃
	dom(subst(e1,x,e2))=dom(e2));

∀e1 x e2.(isextform(e1)∧isvar(x)∧isextform(e2)∧dom(e1)=dom(x) ⊃
	vars(subst(e1,x,e2))⊂vars(e1)∪(vars(e2)-{x}));

∀e1 x e2.(isextform(e1)∧isvar(x)∧isextform(e2)∧dom(e1)=dom(x) ⊃
	∀s.(isstate(s)∧vars(subst(e1,x,e2)⊂domain(s)
		⊃ value(subst(e1,x,e2),s) = value(e2,assign(x,value(e1,s),s))));

CONVERT:

∀x e1 e2.(isvar(x)∧isextform(e1)∧isextform(e2)∧dom(x)=dom(e2)
	⊃ ap2(lambda(x,e),e2)=subst(e2,x,e1));

FORMINDUCTION:

∀x.(isvar(x)⊃P(x)) ∧
∀x y.(xεy ⊃ P(mkconst(x,y))) ∧
∀f e u v.(isextform(f)∧isextform(e)∧dom(f)=(u→v)∧dom(e)=v∧P(f)∧P(e)⊃P(ap2(f,e))) ∧
∀x e.(isvar(x)∧isextform(e)∧P(e) ⊃ P(lambda(x,e))
	⊃ ∀e.(isextform(e) ⊃ P(e));